Nuprl Lemma : q-between_wf
11,40
postcript
pdf
a
,
b
,
c
:
.
a
<
b
<
c
latex
Definitions
P
&
Q
,
a
<
b
<
c
,
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
rationals
wf
,
qless
wf
origin
a, b, c:
. a < b < c 
a, b, c:. a < b < c Tx:A. B(x)